\begin{tabbing}
Konig($k$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$${\it tree}$:(($n$:$\mathbb{N}$ $\times$ (\{0..$n$$^{-}$\}$\rightarrow$\{0..$k$$^{-}$\}))$\rightarrow\mathbb{B}$).\+
\\[0ex]($\forall$$i$:$\mathbb{N}$, $j$:$\mathbb{N}$.
\\[0ex]($i$ $\leq$ $j$) $\Rightarrow$ ($\forall$$x$:(\{0..$j$$^{-}$\}$\rightarrow$\{0..$k$$^{-}$\}). ($\uparrow$(${\it tree}$($<$$j$, $x$$>$))) $\Rightarrow$ ($\uparrow$(${\it tree}$($<$$i$, $x$$>$)))))
\\[0ex]$\Rightarrow$ ($\neg$($\exists$$b$:$\mathbb{N}$. ($\forall$$x$:(\{0..$b$$^{-}$\}$\rightarrow$\{0..$k$$^{-}$\}). $\neg$($\uparrow$(${\it tree}$($<$$b$, $x$$>$))))))
\\[0ex]$\Rightarrow$ ($\exists$$s$:$\mathbb{N}\rightarrow$\{0..$k$$^{-}$\}. ($\forall$$n$:$\mathbb{N}$. $\uparrow$(${\it tree}$($<$$n$, $s$$>$))))
\-
\end{tabbing}